Vardi, M.Y., Verification of concurrent programs: the automata-theoretic framework, Annals of Pure and Applied Logic 51 79–98. We present an automata-theoretic framework to the verification of concurrent and nondeterministic programs. The basic idea is that to verify that a program P is correct one writes a program A that receives the computation of P as input and diverges only on incorrect computations of P. Now P is correct if and only if a program PA, obtained by combining P and (...) A, terminates. We formalize this idea in a framework of ω-automata with a recursive set of states. This unifies previous works on verification of fair termination and verification of temporal properties. (shrink)

Review of Joseph Y. Halpern (ed.), Theoretical Aspects of Reasoning About Knowledge: Proceedings of the 1986 Conference (Los Altos, CA: Morgan Kaufmann, 1986),.

What is an inference rule? This question does not have a unique answer. One usually finds two distinct standard answers in the literature; validity inference $(\sigma \vdash_\mathrm{v} \varphi$ if for every substitution $\tau$, the validity of $\tau \lbrack\sigma\rbrack$ entails the validity of $\tau\lbrack\varphi\rbrack)$, and truth inference $(\sigma \vdash_\mathrm{t} \varphi$ if for every substitution $\tau$, the truth of $\tau\lbrack\sigma\rbrack$ entails the truth of $\tau\lbrack\varphi\rbrack)$. In this paper we introduce a general semantic framework that allows us to investigate the notion of inference (...) more carefully. Validity inference and truth inference are in some sense the extremal points in our framework. We investigate the relationship between various types of inference in our general framework, and consider the complexity of deciding if an inference rule is sound, in the context of a number of logics of interest: classical propositional logic, a nonstandard propositional logic, various propositional modal logics, and first-order logic. (shrink)

In program synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. When the system is open, then at each moment it reads input signals and writes output signals, which depend on the input signals and the history of the computation so far. The specification considers all possible input sequences. Thus, if the specification is linear, it should hold in every computation generated by the interaction, and if the specification is branching, it should hold in (...) the tree that embodies all possible input sequences. Often, the system cannot read all the input signals generated by its environment. For example, in a distributed setting, it might be that each process can read input signals of only part of the underlying processes. Then, we should transform a specification into a system whose output depends only on the readable parts of the input signals and the history of the computation. This is called synthesis with incomplete information. In this work we solve the problem of synthesis with incomplete information in its full generality. We consider linear and branching settings with complete and incomplete information. We claim that alternation is a suitable and helpful mechanism for coping with incomplete information. Using alternating tree automata, we show that incomplete information does not make the synthesis problem more complex, in both the linear and the branching paradigm. In particular, we prove that independently of the presence of incomplete information, the synthesis problems for CTL and CTL * are complete for EXPTIME and 2EXPTIME, respectively. (shrink)

Following increasing public concern over the ethical and social implications of contemporary technology, computer science departments around the world have recently increased their efforts to incorporate ethics into their educational curriculum. For our redesigned undergraduate course on Computer Ethics at Rice University, in addition to teaching variety of fundamental ethical theories and approaches to technology, we also sought to emphasize the role of “social” technologies in mediating moral relations and to encourage students to consider moral decision-making, rather than as an (...) abstract rational process, as matter of affective care. To help us achieve this educational objective and inspired by the work of artist Jenny Odell, we designed an activity for students to practice focusing “deep” attention both on themselves and others. In this article, we describe in detail our rationale for this activity, report on lessons learned, and discuss potential applications for this activity in regard to the ongoing online teaching environment following the Covid-19 pandemic. (shrink)

We identify the computational complexity of the satisfiability problem for FO 2 , the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite (...) model. Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)

In 1960, E. P. Wigner, a joint winner of the 1963 Nobel Prize for Physics, published a paper titled On the Unreasonable Effectiveness of Mathematics in the Natural Sciences [61]. This paper can be construed as an examination and affirmation of Galileo's tenet that “The book of nature is written in the language of mathematics”. To this effect, Wigner presented a large number of examples that demonstrate the effectiveness of mathematics in accurately describing physical phenomena. Wigner viewed these examples as (...) illustrations of what he called the empirical law of epistemology, which asserts that the mathematical formulation of the laws of nature is both appropriate and accurate, and that mathematics is actually the correct language for formulating the laws of nature. At the same time, Wigner pointed out that the reasons for the success of mathematics in the natural sciences are not completely understood; in fact, he went as far as asserting that “… the enormous usefulness of mathematics in the natural sciences is something bordering on the mysterious and there is no rational explanation for it.”. (shrink)

We describe BDD-based decision procedures for the modal logic K. Our approach is inspired by the automata-theoretic approach, but we avoid explicit automata construction. Instead, we compute certain fixpoints of a set of types — which can be viewed as an on-the-fly emptiness of the automaton. We use BDDs to represent and manipulate such type sets, and investigate different kinds of representations as well as a “level-based” representation scheme. The latter turns out to speed up construction and reduce memory consumption (...) considerably. We also study the effect of formula simplification on our decision procedures. To prove the viability of our approach, we compare our approach with a representative selection of other approaches, including a translation of K to QBF. Our results indicate that the BDD-based approach dominates for modally heavy formulae, while search-based approaches dominate for propositionally heavy formulae. (shrink)

In the automata-theoretic approach to verification, we translate specifications to automata. Complexity considerations motivate the distinction between different types of automata. Already in the 60s, it was known that deterministic Büchi word automata are less expressive than nondeterministic Büchi word automata. The proof is easy and can be stated in a few lines. In the late 60s, Rabin proved that Büchi tree automata are less expressive than Rabin tree automata. This proof is much harder. In this work we relate the (...) expressiveness gap between deterministic and nondeterministic Büchi word automata and the expressiveness gap between Büchi and Rabin tree automata. We consider tree automata that recognize derived languages. For a word language L, the derived language of L, denoted L, is the set of all trees all of whose paths are in L. Since often we want to specify that all the computations of the program satisfy some property, the interest in derived languages is clear. Our main result shows that L is recognizable by a nondeterministic Büchi word automaton but not by a deterministic Büchi word automaton iff L is recognizable by a Rabin tree automaton and not by a Büchi tree automaton. Our result provides a simple explanation for the expressiveness gap between Büchi and Rabin tree automata. Since the gap between deterministic and nondeterministic Büchi word automata is well understood, our result also provides a characterization of derived languages that can be recognized by Büchi tree automata. Finally, it also provides an exponential determinization of Büchi tree automata that recognize derived languages. (shrink)

This book gives a comprehensive overview of central themes of finite model theory – expressive power, descriptive complexity, and zero-one laws – together with selected applications relating to database theory and artificial intelligence, especially constraint databases and constraint satisfaction problems. The final chapter provides a concise modern introduction to modal logic, emphasizing the continuity in spirit and technique with finite model theory. This underlying spirit involves the use of various fragments of and hierarchies within first-order, second-order, fixed-point, and infinitary logics (...) to gain insight into phenomena in complexity theory and combinatorics. The book emphasizes the use of combinatorial games, such as extensions and refinements of the Ehrenfeucht-Fraissé pebble game, as a powerful way to analyze the expressive power of such logics, and illustrates how deep notions from model theory and combinatorics, such as o-minimality and treewidth, arise naturally in the application of finite model theory to database theory and AI. Students of logic and computer science will find here the tools necessary to embark on research into finite model theory, and all readers will experience the excitement of a vibrant area of the application of logic to computer science. (shrink)

Reasoning About Knowledge is the first book to provide a general discussion of approaches to reasoning about knowledge and its applications to distributed ...

We interpret the (formal) postulates of measurement in quantum theory in terms of measurement procedures that can be done in the laboratory (at least in principle).

This article isolates ten prepositions, which constitute the undercurrent paradigm of contemporary discourse of health disease and medicine. Discussion of the interrelationship between those prepositions leads to a systematic refutation of this paradigm. An alternative set is being forwarded. The key notions of the existing paradigm are that health is the natural condition of humankind and that disease is a deviance from that nature. Natural things are harmonious and healthy while human made artifacts are coercive interference with natural balance. It (...) is suggested that the current paradigm is influenced by the world of finances and by instrumental reason. The alternative model suggests that human nature cannot be delineated. Humans fashion their own selves and nature by artificial means, medicine among them. The article discusses the implications of the paradigm adapted in various scholarly and popular debates such as the use of sex hormones for contraception, the care of the elderly, holistic medicine and distributive justice in health care. Medicine is not an isolated or a privileged realm. There is no unique entitlement to health care. It is always part of a broader agenda of social values and institutions. A open view of human societies, values and practices as they are situated within concrete material conditions is the platform required for an integrative and creative discourse of health care. (shrink)

The article calls for a departure from the common concept of autonomy in two significant ways: it argues for the supremacy of semantic understanding over procedure, and claims that clinicians are morally obliged to make a strong effort to persuade patients to accept medical advice. We interpret the value of autonomy as derived from the right persons have to respect, as agents who can argue, persuade and be persuaded in matters of utmost personal significance such as decisions about medical care. (...) Hence, autonomy should and could be respected only after such an attempt has been made. Understanding suffering to a significant degree is a prerequisite to sincere efforts of persuasion. It is claimed that a modified and pragmatic form of discourse is the necessary framework for understanding suffering and for compassionately interacting with the frail. (shrink)

Contrary to the common view, this paper suggests that the Hippocratic oath does not directly refer to the controversial subjects of euthanasia and abortion. We interpret the oath in the context of establishing trust in medicine through departure from Pantagruelism. Pantagruelism is coined after Rabelais' classic novel Gargantua and Pantagruel. His satire about a wonder herb, Pantagruelion, is actually a sophisticated model of anti-medicine in which absence of independent moral values and of properly conducted research fashion a flagrant over-medicalization of (...) human problems. Ultimately this undermines the therapeutic core of medicine itself. We contend that PAS is a case of such over-medicalization and that its institution creates medicophobia. This article does not express an opinion about euthanasia in general. Rather, we claim that physicians should learn from the oath and from Rabelais that they should keep their practice to medical care and not to exploit their expertise and social privileges for the sake of ulterior motives, even when their patients desire those goals. (shrink)

If K is an index of relative voting power for simple voting games, the bicameral postulate requires that the distribution of K -power within a voting assembly, as measured by the ratios of the powers of the voters, be independent of whether the assembly is viewed as a separate legislature or as one chamber of a bicameral system, provided that there are no voters common to both chambers. We argue that a reasonable index – if it is to be used (...) as a tool for analysing abstract, ‘uninhabited’ decision rules – should satisfy this postulate. We show that, among known indices, only the Banzhaf measure does so. Moreover, the Shapley–Shubik, Deegan–Packel and Johnston indices sometimes witness a reversal under these circumstances, with voter x ‘less powerful’ than y when measured in the simple voting game G1 , but ‘more powerful’ than y when G1 is ‘bicamerally joined’ with a second chamber G2 . Thus these three indices violate a weaker, and correspondingly more compelling, form of the bicameral postulate. It is also shown that these indices are not always co-monotonic with the Banzhaf index and that as a result they infringe another intuitively plausible condition – the price monotonicity condition. We discuss implications of these findings, in light of recent work showing that only the Shapley–Shubik index, among known measures, satisfies another compelling principle known as the bloc postulate. We also propose a distinction between two separate aspects of voting power: power as share in a fixed purse (P-power) and power as influence (I-power). (shrink)

"In the gorgeous and rugged terrain of Jewish thought, there is no higher mountain to climb than Maimonides, and no more slippery or exhilarating ascent. Halbertal has made it all the way to the top, and his survey of the whole of the Maimonidean landscape is trustworthy and masterful. This is the richest and most intellectually sophisticated book on Maimonides I have ever read."--Leon Wieseltier "In this learned and penetrating work, Halbertal offers us a Maimonides who draws on the dominant (...) Greco-Islamic thought of his time while creating a system of thought that is fully Jewish. He shows us how the early "Commentary on the Mishnah" links up with the "Mishneh Torah" and with the "Guide of the Perplexed," written at the end of his life, to form an unexpected and radical intellectual unity. Beautifully written, "Maimonides" brings out both Maimonides's intellectual success and the paradoxical critical approaches to him after his death."--David J. Wasserstein, Vanderbilt University "Insightful and learned. Halbertal is perhaps the leading philosopher of Jewish law today. His book on Maimonides, like his other writings, reflects wide erudition and is written clearly and sharply."--Warren Zev Harvey, professor emeritus, Hebrew University of Jerusalem "Displaying the marvelous depth and clarity that mark all his work, Halbertal explains in abundant detail the transformations that Maimonides sought to effect in the Jewish world. He provides incisive interpretations of both legal and philosophical writings, yet he is also a biographer, binding together Maimonides's life, self-perception, and intellectual agenda. This is an exceptionally rich book, one that offers fresh perspectives for experts and a highly accessible introduction for general readers."--David Shatz, Yeshiva University "An outstanding and thrilling portrait of Maimonides. Halbertal's analytic lucidity and psychological depth are singular, and his talents are abundantly apparent on every page. This is an extraordinary book."--Menachem Lorberbaum, Tel Aviv University. (shrink)

This book describes Carmeli's cosmological general and special relativity theory, along with Einstein's general and special relativity. These theories are discussed in the context of Moshe Carmeli's original research, in which velocity is introduced as an additional independent dimension. Four- and five-dimensional spaces are considered, and the five-dimensional braneworld theory is presented. The Tully-Fisher law is obtained directly from the theory, and thus it is found that there is no necessity to assume the existence of dark matter in the (...) halo of galaxies, nor in galaxy clusters.The book gives the derivation of the Lorentz transformation, which is used in both Einstein's special relativity and Carmeli's cosmological special relativity theory. The text also provides the mathematical theory of curved space?time geometry, which is necessary to describe both Einstein's general relativity and Carmeli's cosmological general relativity. A comparison between the dynamical and kinematic aspects of the expansion of the universe is made. Comparison is also made between the Friedmann-Robertson-Walker theory and the Carmeli theory. And neither is it necessary to assume the existence of dark matter to correctly describe the expansion of the cosmos. (shrink)

Questionnaire data obtained from 97 supervisory and nonsupervisory employees representing the Production, Production Services, Marketing, and Administration departments of an Israeli metal production plant were used to test the relationship between selected personal and organizational attributes and work related misbehavior. Following Vardi and Wiener''s (1996) framework, Organizational Misbehavior (OMB) was defined as intentional acts that violate formal core organizational rules. We found that there was a significant negative relationship between Organizational Climate and OMB, and between the Organizational Climate dimensions (...) (Warmth and Support, and Reward), and OMB. Also, the activities of misbehavior reported by both managers and employees were negatively related to the Rules, Instrumental and Caring dimensions of Ethical Climates as defined by Victor and Cullen (1988). (shrink)

Annotation. In this volume, the third in his classic series of texts surveying the history of art theory, Moshe Barasch traces the hidden patterns and interlocking themes in the study of art, from Impressionism to Abstract Art. Barasch details the immense social changes in the creation, presentation, and reception of art which have set the history of art theory on a vertiginous new course: the decreased relevance of workshops and art schools; the replacement of the treatise by the critical (...) review; and the interrelation of new modes of scientific inquiry with artistic theory and praxis. The consequent changes in the ways in which critics as well as artists conceptualized paintings and sculptures were radical, marked by an obsession with intense, immediate sensory experiences, psychological reflection on the effects of art, and a magnetic pull to the exotic and alien, making for the most exciting and fertile period in the history of art criticism. (shrink)

Answers to the questions of what justifies conscientious objection in medicine in general and which specific objections should be respected have proven to be elusive. In this paper, I develop a new framework for conscientious objection in medicine that is based on the idea that conscience can express true moral claims. I draw on one of the historical roots, found in Adam Smith’s impartial spectator account, of the idea that an agent’s conscience can determine the correct moral norms, even if (...) the agent’s society has endorsed different norms. In particular, I argue that when a medical professional is reasoning from the standpoint of an impartial spectator, his or her claims of conscience are true, or at least approximate moral truth to the greatest degree possible for creatures like us, and should thus be respected. In addition to providing a justification for conscientious objection in medicine by appealing to the potential truth of the objection, the account advances the debate regarding the integrity and toleration justifications for conscientious objection, since the standard of the impartial spectator specifies the boundaries of legitimate appeals to moral integrity and toleration. The impartial spectator also provides a standpoint of shared deliberation and public reasons, from which a conscientious objector can make their case in terms that other people who adopt this standpoint can and should accept, thus offering a standard fitting to liberal democracies. (shrink)

Physicians frequently ask whether they should give patients what they want, usually when there are considerations pointing against doing so, such as medicine’s values and physicians’ obligations. It has been argued that the source of medicine’s values and physicians’ obligations lies in what has been dubbed “the internal morality of medicine”: medicine is a practice with an end and norms that are definitive of this practice and that determine what physicians ought to do qua physicians. In this paper, I defend (...) the claim that medicine requires a morality that is internal to its practice, while rejecting the prevalent characterization of this morality and offering an alternative one. My approach to the internal morality of medicine is constructivist in nature: the norms of medicine are constructed by medical professionals, other professionals, and patients, given medicine’s end of “benefitting patients in need of prima facie medical treatment and care.” I make the case that patients should be involved in the construction of medicine’s morality not only because they have knowledge that is relevant to the internal morality of medicine—namely, their own values and preferences—but also because medicine is an inherently relational enterprise: in medicine the relationship between physician and patient is a constitutive component of the craft itself. The framework I propose provides an authoritative morality for medicine, while allowing for the incorporation, into that very morality, of qualified deference to patient values. (shrink)

Two problems seem to plague Adam Smith’s account of sympathy and approbation in The Theory of Moral Sentiments (TMS). First, Smith’s account of sympathy at the beginning of TMS appears to be inconsistent with the account of sympathy at the end of TMS. In particular, it seems that Smith did not appreciate the distinction between ‘self-oriented sympathy’ and ‘other-oriented sympathy’, that is, between imagining being oneself in the actor’s situation and imagining being the actor in the actor’s situation. Second, Smith’s (...) account of approbation, according to which a sentiment of approval arises when there is recognition of concordance between the spectator’s sympathetic passion and the actor’s original passion, seems to face the following problem: since the spectator attains both his own sympathetic passion and the actor’s original passion by sympathizing with the actor, the sympathetic passion of the spectator and the original passion of the actor will necessarily be identical. Therefore, Smith’s account of approbation requires that the spectator utilize both self-oriented and other-oriented sympathy (‘the double-sympathy model of approbation’). I offer a novel developmental account of sympathy in TMS that renders Smith’s account of sympathy consistent and allows for the utilization of the double-sympathy model of approbation. (shrink)

My question in the chapter is this: could (and should) the role of the physician be construed as that of a friend to the patient? I begin by briefly discussing the “friendship model” of the physician-patient relationship—according to which physicians and patients could, and perhaps should, be friends—as well as its history and limitations. Given these limitations, I focus on the more one-sided idea that the physician could, and perhaps should, be a friend to the patient (a “physician-qua-friend model” of (...) the physician-patient relationship). I show that given recent developments in our understanding of the physician-patient relationship, this idea is far from asinine. I then make the case that the most plausible conception of the physician-qua-friend model incorporates the following components: (a) a common goal, that is, one that physician and patient share; (b) certain forms of equality between physician and patient; (c) an ideal of a caring physician. Finally, I show how the model can be instantiated in a certain type of physician-patient interaction, namely, in physician-assisted dying. (shrink)

The literature on conscientious objection in medicine presents two key problems that remain unresolved: Which conscientious objections in medicine are justified, if it is not feasible for individual medical practitioners to conclusively demonstrate the genuineness or reasonableness of their objections? How does one respect both medical practitioners’ claims of conscience and patients’ interests, without leaving practitioners complicit in perceived or actual wrongdoing? My aim in this paper is to offer a new framework for conscientious objections in medicine, which, by bringing (...) medical professionals’ conscientious objection into the public realm, solves the justification and complicity problems. In particular, I will argue that: an “Uber Conscientious Objection in Medicine Committee” —which includes representatives from the medical community and from other professions, as well as from various religions and from the patient population—should assess various well-known conscientious objections in medicine in terms of public reason and decide which conscientious objections should be permitted, without hearing out individual conscientious objectors; medical practitioners should advertise their conscientious objections, ahead of time, in an online database that would be easily accessible to the public, without being required, in most cases, to refer patients to non-objecting practitioners. (shrink)

The Humean Theory of Reasons, according to which all of our reasons for action are explained by our desires, has been criticized for not being able to account for “moral reasons,” namely, overriding reasons to act on moral demands regardless of one's desires. My aim in this paper is to utilize ideas from Adam Smith's moral philosophy in order to offer a novel and alternative account of moral reasons that is both desire-based and accommodating of an adequate version of the (...) requirement that moral demands have overriding reason-giving force. In particular, I argue that the standpoint of what Smith calls “the impartial spectator” can both determine what is morally appropriate and inappropriate and provide the basis for normative reasons for action—including reasons to act on moral demands—to nearly all reason-responsive agents and, furthermore, that these reasons have the correct weight. The upshot of the proposed account is that it offers an interesting middle road out of a dilemma pertaining to the explanatory and normative dimensions of reasons for informed-desire Humean theorists. (shrink)

I build on Adam Smith’s account of the impartial spectator in The Theory of Moral Sentiments in order to offer a modest ideal observer theory of moral judgment that is adequate in the following sense: the account specifies the hypothetical conditions that guarantee the authoritativeness of an agent’s (or agents’) responses in constituting the standard in question, and, if an actual agent or an actual community of agents are not under those conditions, their responses are not authoritative in setting this (...) standard. However, in the account that I provide, the hypothetical conditions can themselves be constructed from the psychology and interactions of actual human beings. In other words, facts about the morally appropriate and inappropriate are determined from hypothetical conditions that––while agents in a given society might have yet to attain them––can be constructed from those agents’ shared experiences. Thus, the account offers both an attainable standard of moral judgment and a standard that can transcend the biases of the society which gave rise to it. I also defend the account against three challenges: (a) ideal observer theories do not offer the right kind of motivation to act on the verdicts of the ideal observer; (b) ideal observer theories cannot explain why the idealization in question is well-motivated and not objectionably ad hoc; (c) the standard used in ideal observer theories cannot be defended upon further reflection, because we would need a non-arbitrary, second-order standard to govern our reflection on the first-order standard of moral judgment. (shrink)

I offer a novel two-stage reconstruction of Hume’s general-point-of-view account, modeled in part on his qualified-judges account in ‘Of the Standard of Taste.’ In particular, I argue that the general point of view needs to be jointly constructed by spectators who have sympathized with (at least some of) the agents in (at least some of) the actor’s circles of influence. The upshot of the account is two-fold. First, Hume’s later thought developed in such a way that it can rectify the (...) problems inherent in his Treatise account of the general point of view. Second, the proposed account provides the grounds for an adequate and well-motivated modest ideal observer theory of the standard of virtue. (shrink)